T:Type, L:T List, P:(||L||), x:T. (x  filter2(P;L))  (i:||L||. x = L[i] & P(i)) 

latex

Definitions	b, t  T, x:A. B(x), , A & B, x:A. B(x), {i..j}, P & Q, , i  j < k, ||as||, P  Q, False, A, AB, Prop, l[i], P  Q, P  Q, (x  l), b, ij, Unit, True, T, {T}, SQType(T), P  Q, Dec(P), filter2(P;L), hd(l), i<j, ij
Lemmas	iff functionality wrt iff, select cons tl, filter2 wf, le wf, decidable int equal, iff wf, l member wf, squash wf, true wf, cons filter2, length cons, length wf1, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, non neg length, bnot wf, not wf, nat wf, length wf2, select wf, assert wf, int seg wf, bool wf